\begin{tabbing}
$\forall$\=${\it es}$:ES, $C$, $T$:Type, $S$:($C$$\rightarrow$$C$$\rightarrow$E$\rightarrow\mathbb{P}$), $R$:($C$$\rightarrow$E$\rightarrow\mathbb{P}$),\+
\\[0ex]${\it codes}$:($j$,$i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $S$($j$,$i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$),
\\[0ex]${\it decodes}$:($i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $R$($i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$), ${\it Req}$:($C$$\rightarrow$E$\rightarrow\mathbb{P}$), ${\it Ack}$:($C$$\rightarrow$$C$$\rightarrow$E$\rightarrow\mathbb{P}$), $i$:$C$,
\\[0ex]$f$:(\{$e$:E$\mid$ $R$($i$,$e$)\} $\rightarrow$\{$e$:E$\mid$ $\exists$$j$:$C$. ($S$($j$,$i$,$e$))\} ).
\-\\[0ex]fifo+property(${\it es}$;${\it codes}$;${\it decodes}$;$C$;$S$;$R$;$T$;${\it Req}$;${\it Ack}$;$i$;$f$) $\in$ $\mathbb{P}$
\end{tabbing}